WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            choice(dd(u,S),K,E) -> choice(S,K,E)
            choice(dd(u,S),K,E) -> choice(S,dd(u,K),E)
            choice(nil(),K,E) -> ite(clique(K,E),K,nil())
            clique(dd(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff())
            clique(nil(),E) -> tt()
            complete(u,dd(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff())
            complete(u,nil(),E) -> tt()
            find(u,v,dd(dd(u,v),E)) -> tt()
            find(u,v,dd(dd(u2,v2),E)) -> find(u,v,E)
            find(u,v,nil()) -> ff()
            ite(ff(),u,v) -> v
            ite(tt(),u,v) -> u
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3} / {dd/2,ff/0,nil/0,tt/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice,clique,complete,find,ite} and constructors {dd,ff
            ,nil,tt}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
          choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
          choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
          clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
          clique#(nil(),E) -> c_5()
          complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
          complete#(u,nil(),E) -> c_7()
          find#(u,v,dd(dd(u,v),E)) -> c_8()
          find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
          find#(u,v,nil()) -> c_10()
          ite#(ff(),u,v) -> c_11()
          ite#(tt(),u,v) -> c_12()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
            clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
            clique#(nil(),E) -> c_5()
            complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
            complete#(u,nil(),E) -> c_7()
            find#(u,v,dd(dd(u,v),E)) -> c_8()
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
            find#(u,v,nil()) -> c_10()
            ite#(ff(),u,v) -> c_11()
            ite#(tt(),u,v) -> c_12()
        - Weak TRS:
            choice(dd(u,S),K,E) -> choice(S,K,E)
            choice(dd(u,S),K,E) -> choice(S,dd(u,K),E)
            choice(nil(),K,E) -> ite(clique(K,E),K,nil())
            clique(dd(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff())
            clique(nil(),E) -> tt()
            complete(u,dd(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff())
            complete(u,nil(),E) -> tt()
            find(u,v,dd(dd(u,v),E)) -> tt()
            find(u,v,dd(dd(u2,v2),E)) -> find(u,v,E)
            find(u,v,nil()) -> ff()
            ite(ff(),u,v) -> v
            ite(tt(),u,v) -> u
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/2,c_4/3,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {5,7,8,10,11,12}
        by application of
          Pre({5,7,8,10,11,12}) = {3,4,6,9}.
        Here rules are labelled as follows:
          1: choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
          2: choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
          3: choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
          4: clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
          5: clique#(nil(),E) -> c_5()
          6: complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
          7: complete#(u,nil(),E) -> c_7()
          8: find#(u,v,dd(dd(u,v),E)) -> c_8()
          9: find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
          10: find#(u,v,nil()) -> c_10()
          11: ite#(ff(),u,v) -> c_11()
          12: ite#(tt(),u,v) -> c_12()
* Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
            clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
            complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        - Weak DPs:
            clique#(nil(),E) -> c_5()
            complete#(u,nil(),E) -> c_7()
            find#(u,v,dd(dd(u,v),E)) -> c_8()
            find#(u,v,nil()) -> c_10()
            ite#(ff(),u,v) -> c_11()
            ite#(tt(),u,v) -> c_12()
        - Weak TRS:
            choice(dd(u,S),K,E) -> choice(S,K,E)
            choice(dd(u,S),K,E) -> choice(S,dd(u,K),E)
            choice(nil(),K,E) -> ite(clique(K,E),K,nil())
            clique(dd(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff())
            clique(nil(),E) -> tt()
            complete(u,dd(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff())
            complete(u,nil(),E) -> tt()
            find(u,v,dd(dd(u,v),E)) -> tt()
            find(u,v,dd(dd(u2,v2),E)) -> find(u,v,E)
            find(u,v,nil()) -> ff()
            ite(ff(),u,v) -> v
            ite(tt(),u,v) -> u
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/2,c_4/3,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
             -->_1 choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E)):3
             -->_1 choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E)):2
             -->_1 choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E)):1
          
          2:S:choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
             -->_1 choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E)):3
             -->_1 choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E)):2
             -->_1 choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E)):1
          
          3:S:choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
             -->_2 clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E)):4
             -->_1 ite#(tt(),u,v) -> c_12():12
             -->_1 ite#(ff(),u,v) -> c_11():11
             -->_2 clique#(nil(),E) -> c_5():7
          
          4:S:clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
             -->_2 complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff())
                                                ,find#(u,v,E)
                                                ,complete#(u,S,E)):5
             -->_1 ite#(tt(),u,v) -> c_12():12
             -->_1 ite#(ff(),u,v) -> c_11():11
             -->_2 complete#(u,nil(),E) -> c_7():8
             -->_3 clique#(nil(),E) -> c_5():7
             -->_3 clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E)):4
          
          5:S:complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
             -->_2 find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E)):6
             -->_1 ite#(tt(),u,v) -> c_12():12
             -->_1 ite#(ff(),u,v) -> c_11():11
             -->_2 find#(u,v,nil()) -> c_10():10
             -->_2 find#(u,v,dd(dd(u,v),E)) -> c_8():9
             -->_3 complete#(u,nil(),E) -> c_7():8
             -->_3 complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E)):5
          
          6:S:find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
             -->_1 find#(u,v,nil()) -> c_10():10
             -->_1 find#(u,v,dd(dd(u,v),E)) -> c_8():9
             -->_1 find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E)):6
          
          7:W:clique#(nil(),E) -> c_5()
             
          
          8:W:complete#(u,nil(),E) -> c_7()
             
          
          9:W:find#(u,v,dd(dd(u,v),E)) -> c_8()
             
          
          10:W:find#(u,v,nil()) -> c_10()
             
          
          11:W:ite#(ff(),u,v) -> c_11()
             
          
          12:W:ite#(tt(),u,v) -> c_12()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          7: clique#(nil(),E) -> c_5()
          8: complete#(u,nil(),E) -> c_7()
          11: ite#(ff(),u,v) -> c_11()
          12: ite#(tt(),u,v) -> c_12()
          9: find#(u,v,dd(dd(u,v),E)) -> c_8()
          10: find#(u,v,nil()) -> c_10()
* Step 4: SimplifyRHS WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
            clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
            complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        - Weak TRS:
            choice(dd(u,S),K,E) -> choice(S,K,E)
            choice(dd(u,S),K,E) -> choice(S,dd(u,K),E)
            choice(nil(),K,E) -> ite(clique(K,E),K,nil())
            clique(dd(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff())
            clique(nil(),E) -> tt()
            complete(u,dd(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff())
            complete(u,nil(),E) -> tt()
            find(u,v,dd(dd(u,v),E)) -> tt()
            find(u,v,dd(dd(u2,v2),E)) -> find(u,v,E)
            find(u,v,nil()) -> ff()
            ite(ff(),u,v) -> v
            ite(tt(),u,v) -> u
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/2,c_4/3,c_5/0,c_6/3,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
             -->_1 choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E)):3
             -->_1 choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E)):2
             -->_1 choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E)):1
          
          2:S:choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
             -->_1 choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E)):3
             -->_1 choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E)):2
             -->_1 choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E)):1
          
          3:S:choice#(nil(),K,E) -> c_3(ite#(clique(K,E),K,nil()),clique#(K,E))
             -->_2 clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E)):4
          
          4:S:clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E))
             -->_2 complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff())
                                                ,find#(u,v,E)
                                                ,complete#(u,S,E)):5
             -->_3 clique#(dd(u,K),E) -> c_4(ite#(complete(u,K,E),clique(K,E),ff()),complete#(u,K,E),clique#(K,E)):4
          
          5:S:complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E))
             -->_2 find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E)):6
             -->_3 complete#(u,dd(v,S),E) -> c_6(ite#(find(u,v,E),complete(u,S,E),ff()),find#(u,v,E),complete#(u,S,E)):5
          
          6:S:find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
             -->_1 find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E)):6
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          choice#(nil(),K,E) -> c_3(clique#(K,E))
          clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
          complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
* Step 5: UsableRules WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(clique#(K,E))
            clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
            complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        - Weak TRS:
            choice(dd(u,S),K,E) -> choice(S,K,E)
            choice(dd(u,S),K,E) -> choice(S,dd(u,K),E)
            choice(nil(),K,E) -> ite(clique(K,E),K,nil())
            clique(dd(u,K),E) -> ite(complete(u,K,E),clique(K,E),ff())
            clique(nil(),E) -> tt()
            complete(u,dd(v,S),E) -> ite(find(u,v,E),complete(u,S,E),ff())
            complete(u,nil(),E) -> tt()
            find(u,v,dd(dd(u,v),E)) -> tt()
            find(u,v,dd(dd(u2,v2),E)) -> find(u,v,E)
            find(u,v,nil()) -> ff()
            ite(ff(),u,v) -> v
            ite(tt(),u,v) -> u
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
          choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
          choice#(nil(),K,E) -> c_3(clique#(K,E))
          clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
          complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
          find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
* Step 6: DecomposeDG WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(clique#(K,E))
            clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
            complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
          choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
          choice#(nil(),K,E) -> c_3(clique#(K,E))
          clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
        and a lower component
          complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
          find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        Further, following extension rules are added to the lower component.
          choice#(dd(u,S),K,E) -> choice#(S,K,E)
          choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
          choice#(nil(),K,E) -> clique#(K,E)
          clique#(dd(u,K),E) -> clique#(K,E)
          clique#(dd(u,K),E) -> complete#(u,K,E)
** Step 6.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(clique#(K,E))
            clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
             -->_1 choice#(nil(),K,E) -> c_3(clique#(K,E)):3
             -->_1 choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E)):2
             -->_1 choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E)):1
          
          2:S:choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
             -->_1 choice#(nil(),K,E) -> c_3(clique#(K,E)):3
             -->_1 choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E)):2
             -->_1 choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E)):1
          
          3:S:choice#(nil(),K,E) -> c_3(clique#(K,E))
             -->_1 clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E)):4
          
          4:S:clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E))
             -->_2 clique#(dd(u,K),E) -> c_4(complete#(u,K,E),clique#(K,E)):4
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          clique#(dd(u,K),E) -> c_4(clique#(K,E))
** Step 6.a:2: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(clique#(K,E))
            clique#(dd(u,K),E) -> c_4(clique#(K,E))
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(0)
          choice# :: ["A"(0) x "A"(0) x "A"(0)] -(1)-> "A"(0)
          clique# :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(0)
          c_2 :: ["A"(0)] -(0)-> "A"(0)
          c_3 :: ["A"(0)] -(0)-> "A"(0)
          c_4 :: ["A"(0)] -(0)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
        
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          choice#(nil(),K,E) -> c_3(clique#(K,E))
        2. Weak:
          choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
          choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
          clique#(dd(u,K),E) -> c_4(clique#(K,E))
** Step 6.a:3: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            clique#(dd(u,K),E) -> c_4(clique#(K,E))
        - Weak DPs:
            choice#(nil(),K,E) -> c_3(clique#(K,E))
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          dd :: ["A"(0) x "A"(13)] -(13)-> "A"(13)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(13)
          choice# :: ["A"(13) x "A"(0) x "A"(14)] -(1)-> "A"(0)
          clique# :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(14)
          c_2 :: ["A"(0)] -(0)-> "A"(0)
          c_3 :: ["A"(0)] -(0)-> "A"(0)
          c_4 :: ["A"(0)] -(0)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_2_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_4_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
        2. Weak:
          choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
          clique#(dd(u,K),E) -> c_4(clique#(K,E))
** Step 6.a:4: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            clique#(dd(u,K),E) -> c_4(clique#(K,E))
        - Weak DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(nil(),K,E) -> c_3(clique#(K,E))
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          dd :: ["A"(0) x "A"(15)] -(15)-> "A"(15)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          nil :: [] -(0)-> "A"(15)
          choice# :: ["A"(15) x "A"(0) x "A"(14)] -(5)-> "A"(0)
          clique# :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(14)
          c_2 :: ["A"(0)] -(0)-> "A"(14)
          c_3 :: ["A"(0)] -(0)-> "A"(0)
          c_4 :: ["A"(0)] -(0)-> "A"(14)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_2_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_4_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
        2. Weak:
          clique#(dd(u,K),E) -> c_4(clique#(K,E))
** Step 6.a:5: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            clique#(dd(u,K),E) -> c_4(clique#(K,E))
        - Weak DPs:
            choice#(dd(u,S),K,E) -> c_1(choice#(S,K,E))
            choice#(dd(u,S),K,E) -> c_2(choice#(S,dd(u,K),E))
            choice#(nil(),K,E) -> c_3(clique#(K,E))
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/1,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          dd :: ["A"(0) x "A"(4)] -(4)-> "A"(4)
          dd :: ["A"(0) x "A"(12)] -(12)-> "A"(12)
          nil :: [] -(0)-> "A"(12)
          choice# :: ["A"(12) x "A"(4) x "A"(14)] -(2)-> "A"(0)
          clique# :: ["A"(4) x "A"(0)] -(2)-> "A"(0)
          c_1 :: ["A"(0)] -(0)-> "A"(0)
          c_2 :: ["A"(0)] -(0)-> "A"(14)
          c_3 :: ["A"(0)] -(0)-> "A"(14)
          c_4 :: ["A"(0)] -(0)-> "A"(12)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_1_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_2_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_3_A" :: ["A"(0)] -(0)-> "A"(1)
          "c_4_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          clique#(dd(u,K),E) -> c_4(clique#(K,E))
        2. Weak:
          

** Step 6.b:1: DecomposeDG WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict DPs:
            complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        - Weak DPs:
            choice#(dd(u,S),K,E) -> choice#(S,K,E)
            choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
            choice#(nil(),K,E) -> clique#(K,E)
            clique#(dd(u,K),E) -> clique#(K,E)
            clique#(dd(u,K),E) -> complete#(u,K,E)
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing}
    + Details:
        We decompose the input problem according to the dependency graph into the upper component
          choice#(dd(u,S),K,E) -> choice#(S,K,E)
          choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
          choice#(nil(),K,E) -> clique#(K,E)
          clique#(dd(u,K),E) -> clique#(K,E)
          clique#(dd(u,K),E) -> complete#(u,K,E)
          complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
        and a lower component
          find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        Further, following extension rules are added to the lower component.
          choice#(dd(u,S),K,E) -> choice#(S,K,E)
          choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
          choice#(nil(),K,E) -> clique#(K,E)
          clique#(dd(u,K),E) -> clique#(K,E)
          clique#(dd(u,K),E) -> complete#(u,K,E)
          complete#(u,dd(v,S),E) -> complete#(u,S,E)
          complete#(u,dd(v,S),E) -> find#(u,v,E)
*** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
        - Weak DPs:
            choice#(dd(u,S),K,E) -> choice#(S,K,E)
            choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
            choice#(nil(),K,E) -> clique#(K,E)
            clique#(dd(u,K),E) -> clique#(K,E)
            clique#(dd(u,K),E) -> complete#(u,K,E)
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        SimplifyRHS
    + Details:
        Consider the dependency graph
          1:S:complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E))
             -->_2 complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E)):1
          
          2:W:choice#(dd(u,S),K,E) -> choice#(S,K,E)
             -->_1 choice#(nil(),K,E) -> clique#(K,E):4
             -->_1 choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E):3
             -->_1 choice#(dd(u,S),K,E) -> choice#(S,K,E):2
          
          3:W:choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
             -->_1 choice#(nil(),K,E) -> clique#(K,E):4
             -->_1 choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E):3
             -->_1 choice#(dd(u,S),K,E) -> choice#(S,K,E):2
          
          4:W:choice#(nil(),K,E) -> clique#(K,E)
             -->_1 clique#(dd(u,K),E) -> complete#(u,K,E):6
             -->_1 clique#(dd(u,K),E) -> clique#(K,E):5
          
          5:W:clique#(dd(u,K),E) -> clique#(K,E)
             -->_1 clique#(dd(u,K),E) -> complete#(u,K,E):6
             -->_1 clique#(dd(u,K),E) -> clique#(K,E):5
          
          6:W:clique#(dd(u,K),E) -> complete#(u,K,E)
             -->_1 complete#(u,dd(v,S),E) -> c_6(find#(u,v,E),complete#(u,S,E)):1
          
        Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
          complete#(u,dd(v,S),E) -> c_6(complete#(u,S,E))
*** Step 6.b:1.a:2: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            complete#(u,dd(v,S),E) -> c_6(complete#(u,S,E))
        - Weak DPs:
            choice#(dd(u,S),K,E) -> choice#(S,K,E)
            choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
            choice#(nil(),K,E) -> clique#(K,E)
            clique#(dd(u,K),E) -> clique#(K,E)
            clique#(dd(u,K),E) -> complete#(u,K,E)
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/1,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          dd :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          nil :: [] -(0)-> "A"(1)
          choice# :: ["A"(1) x "A"(1) x "A"(14)] -(3)-> "A"(0)
          clique# :: ["A"(1) x "A"(0)] -(1)-> "A"(1)
          complete# :: ["A"(0) x "A"(1) x "A"(0)] -(0)-> "A"(4)
          c_6 :: ["A"(0)] -(0)-> "A"(6)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_6_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          complete#(u,dd(v,S),E) -> c_6(complete#(u,S,E))
        2. Weak:
          

*** Step 6.b:1.b:1: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        - Weak DPs:
            choice#(dd(u,S),K,E) -> choice#(S,K,E)
            choice#(dd(u,S),K,E) -> choice#(S,dd(u,K),E)
            choice#(nil(),K,E) -> clique#(K,E)
            clique#(dd(u,K),E) -> clique#(K,E)
            clique#(dd(u,K),E) -> complete#(u,K,E)
            complete#(u,dd(v,S),E) -> complete#(u,S,E)
            complete#(u,dd(v,S),E) -> find#(u,v,E)
        - Signature:
            {choice/3,clique/2,complete/3,find/3,ite/3,choice#/3,clique#/2,complete#/3,find#/3,ite#/3} / {dd/2,ff/0
            ,nil/0,tt/0,c_1/1,c_2/1,c_3/1,c_4/2,c_5/0,c_6/2,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {choice#,clique#,complete#,find#
            ,ite#} and constructors {dd,ff,nil,tt}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          dd :: ["A"(0) x "A"(9)] -(9)-> "A"(9)
          dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8)
          nil :: [] -(0)-> "A"(8)
          choice# :: ["A"(8) x "A"(0) x "A"(14)] -(13)-> "A"(0)
          clique# :: ["A"(0) x "A"(12)] -(1)-> "A"(7)
          complete# :: ["A"(0) x "A"(0) x "A"(10)] -(1)-> "A"(8)
          find# :: ["A"(0) x "A"(0) x "A"(9)] -(1)-> "A"(8)
          c_9 :: ["A"(0)] -(0)-> "A"(14)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_9_A" :: ["A"(0)] -(0)-> "A"(1)
          "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "nil_A" :: [] -(0)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          find#(u,v,dd(dd(u2,v2),E)) -> c_9(find#(u,v,E))
        2. Weak:
          

WORST_CASE(?,O(n^3))